es:ES, e:E.
((first(e)))
 ((discrete state after pred(e)) = (discrete state when e)  discrete state@loc(e)) 

latex

Definitions

t  T, x:A. B(x), (discrete state when e), discrete state@i, Id, Type, Top, if b then t else f fi , x:AB(x), s = t, P  Q, (discrete state after e), x:A  B(x), ES, let x,y = A in B(x;y), t.1, E, False, A, <a, b>, {T}, SQType(T), (timed)state after e, , Void, x:A.B(x), b, b, , Atom$n, es_state_when(es;e), discrete(i;x), P & Q, P  Q, Unit, left + right, , x when e, (x after e), s+r, es_state(es;i), first(e), loc(e), pred(e), s ~ t, vartype(i;x), f(a), state@i, s(now), A c B, case b of inl(x) => s(x) | inr(y) => t(y), s.x, , , time(e), r - s, #$n, r + s

Lemmas

es-isconst-property, int-rational, qadd wf, int inc rationals, qsub wf, es-time wf, es-first wf, es-E wf, event system wf, state-after-pred, es-read-state wf, es state wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-isconst wf, bool wf, bnot wf, not wf, assert wf, es-vartype wf, es-loc wf, Id wf, Id sq, es-loc-pred, es-dstate-after wf, es-pred wf, es-dstate-when wf